| 1: | fact(X) | → if(zero(X),n__s(n__0),n__prod(X,n__fact(n__p(X)))) | |
| 2: | add(0,X) | → X | |
| 3: | add(s(X),Y) | → s(add(X,Y)) | |
| 4: | prod(0,X) | → 0 | |
| 5: | prod(s(X),Y) | → add(Y,prod(X,Y)) | |
| 6: | if(true,X,Y) | → activate(X) | |
| 7: | if(false,X,Y) | → activate(Y) | |
| 8: | zero(0) | → true | |
| 9: | zero(s(X)) | → false | |
| 10: | p(s(X)) | → X | |
| 11: | s(X) | → n__s(X) | |
| 12: | 0 | → n__0 | |
| 13: | prod(X1,X2) | → n__prod(X1,X2) | |
| 14: | fact(X) | → n__fact(X) | |
| 15: | p(X) | → n__p(X) | |
| 16: | activate(n__s(X)) | → s(activate(X)) | |
| 17: | activate(n__0) | → 0 | |
| 18: | activate(n__prod(X1,X2)) | → prod(activate(X1),activate(X2)) | |
| 19: | activate(n__fact(X)) | → fact(activate(X)) | |
| 20: | activate(n__p(X)) | → p(activate(X)) | |
| 21: | activate(X) | → X | |
| 22: | FACT(X) | → IF(zero(X),n__s(n__0),n__prod(X,n__fact(n__p(X)))) | |
| 23: | FACT(X) | → ZERO(X) | |
| 24: | ADD(s(X),Y) | → S(add(X,Y)) | |
| 25: | ADD(s(X),Y) | → ADD(X,Y) | |
| 26: | PROD(s(X),Y) | → ADD(Y,prod(X,Y)) | |
| 27: | PROD(s(X),Y) | → PROD(X,Y) | |
| 28: | IF(true,X,Y) | → ACTIVATE(X) | |
| 29: | IF(false,X,Y) | → ACTIVATE(Y) | |
| 30: | ACTIVATE(n__s(X)) | → S(activate(X)) | |
| 31: | ACTIVATE(n__s(X)) | → ACTIVATE(X) | |
| 32: | ACTIVATE(n__0) | → 0# | |
| 33: | ACTIVATE(n__prod(X1,X2)) | → PROD(activate(X1),activate(X2)) | |
| 34: | ACTIVATE(n__prod(X1,X2)) | → ACTIVATE(X1) | |
| 35: | ACTIVATE(n__prod(X1,X2)) | → ACTIVATE(X2) | |
| 36: | ACTIVATE(n__fact(X)) | → FACT(activate(X)) | |
| 37: | ACTIVATE(n__fact(X)) | → ACTIVATE(X) | |
| 38: | ACTIVATE(n__p(X)) | → P(activate(X)) | |
| 39: | ACTIVATE(n__p(X)) | → ACTIVATE(X) | |